1  {x}={c|xεV∧c=x}    ∀E UNIT x
2  ∃y.∀a.(aεy≡a⊂x)    ∀E KPOWER x
3  ∀a.(aεy≡a⊂x)  (3)  ∃E 2 (y)
4  xεy≡x⊂x  (3)  ∀E 3 x
5  x⊂x≡∀c.(cεx⊃cεx)    ∀E SUBSET x,x
6  cεx⊃cεx    TAUT cεx⊃cεx 
7  ∀c.(cεx⊃cεx)    ∀I 6 c
8  {x}⊂y≡∀c.(cε{x}⊃cεy)    ∀E SUBSET {x},y
9  cε{x}  (9)  ASSUME 
10  ∀a.(aε{b|xεV∧b=x}≡(SET(a)∧(xεV∧a=x)))    ∧I KCOMP
11  cε{b|xεV∧b=x}≡(SET(c)∧(xεV∧c=x))    ∀E 10 c
12  {x}={b|xεV∧b=x}    TAUTEQ {x}={b|xεV∧b=x} 1
13  cε{x}≡(SET(c)∧(xεV∧c=x))    SUBST 12 IN 11
14  c=x  (9)  TAUT c=x 9,13
15  cε{x}⊃c=x    ⊃I 9⊃14
16  cε{x}⊃cεy  (3)  TAUTEQ cε{x}⊃cεy 4:5,7,15
17  ∀c.(cε{x}⊃cεy)  (3)  ∀I 16 c
18  {x}⊂y  (3)  TAUT {x}⊂y 8,17
19  ∃y1.∀a.(aεy1≡a⊂y)    ∀E KPOWER y
20  ∀a.(aεy1≡a⊂y)  (20)  ∃E 19 (y1)
21  {x}εy1≡{x}⊂y  (20)  ∀E 20 {x}
22  {x}εy1  (3 20)  TAUT {x}εy1 18,21
23  ∃b.{x}εb    ∃I 22 y1←b
24  SET({x})≡∃b.{x}εb    ∀E SET {x}
25  SET({x})    TAUT SET({x}) 23:24
26  ∀x.SET({x})    ∀I 25 x